\begin{tabbing}
$\forall$\=$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+\+
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)\} ,
\-\\[0ex]$v$:$T$.
\-\\[0ex]($\uparrow$$x$ changed before $e$) $\Rightarrow$ (es{-}when(${\it es}$; $x$; $e$) = $v$) $\Rightarrow$ @(last change to $x$ before $e$)($x$$\rightarrow$$v$)
\end{tabbing}